/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package simhya.modelchecking.mtl;



/**
 *
 * @author Luca
 */
public class MTLuntil  extends MTLmodalNode {
    
    public MTLuntil(MTLnode left, MTLnode right) {
        super(new ParametricInterval());
        super.setChildren(left,right);
        left.setParent(this);
        right.setParent(this);
    }

    public MTLuntil(ParametricInterval interval, MTLnode left, MTLnode right) {
        super(interval);
        super.setChildren(left,right);
        left.setParent(this);
        right.setParent(this);
    }
    
    @Override
    public String toFormulaTree(int depth) {
        String s = "";
        for (int i=0;i<depth;i++)
            s += "   ";
        s += "Until " + parametricInterval.toString() + "\n";
        return s + super.toFormulaTree(depth);
    }
    
    @Override
    boolean checkGoal(int j) {
        if (j < this.traceLength) 
            return right.truthValue[j];
        else return false;
    }

    @Override
    boolean checkSafe(int j) {
        if (j < this.traceLength) 
            return left.truthValue[j];
        else return false;
    }

    @Override
    void setBad(int i) {
        this.truthValue[i] = false;
    }

    @Override
    void setOk(int i) {
        this.truthValue[i] = true;
    }
   
}
